Inference at * 1 0 
Iof proof for Lemma eq int cases test:



1. A : Type
2. x : A
3. y : A
4. P : A
5. i : 
6. j : 
7. P(if (i = j) then x else y fi )
  P(if (i = j) then x else y fi ) 

latex

 by (%S% 
\p. 
\plet UA = get_term_arg `UA` p 
\pin let A = get_term_arg `A` p 

\pinin let e = get_term_arg `e` p 
\pin let x = get_term_arg `x` p 
\pin 
\piAssertL 

\piAsse[mk_member_term UA A 
\piAs;mk_member_term A e 
\piAs;mk_all_term (dv x) A (mk_member_term 

\piAs;mk_all_term (dv x) A (mk_meUA (mk_equal_term A e x)) 
\piAs] 
\pip) 

latex

\p1: .....assertion..... NILNIL

\p1:     Type
\p2: .....assertion..... NILNIL

\p2: 8.   Type
\p2:   (i = j)  
\p3: .....assertion..... NILNIL

\p3: 8.   Type
\p3: 9. (i = j)  
\p3:   bb:. ((i = j) = bb)  Type
\p4: 

\p4: 8.   Type
\p4: 9. (i = j)  
\p4: 10. bb:. ((i = j) = bb)  Type
\p4:   P(if (i = j) then x else y fi )
\p.

Definitions

, t  T, (i = j), if b then t else f fi , f(a), , , x:AB(x), Type